0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 386 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 80 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 201 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 39 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 4 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 Narrowing (⇒, 0 ms)
↳43 QDP
↳44 UsableRulesProof (⇔, 0 ms)
↳45 QDP
↳46 QReductionProof (⇔, 0 ms)
↳47 QDP
↳48 Instantiation (⇔, 0 ms)
↳49 QDP
↳50 DependencyGraphProof (⇔, 0 ms)
↳51 QDP
↳52 QDPQMonotonicMRRProof (⇔, 906 ms)
↳53 QDP
↳54 UsableRulesProof (⇔, 0 ms)
↳55 QDP
↳56 QReductionProof (⇔, 2 ms)
↳57 QDP
↳58 Narrowing (⇒, 0 ms)
↳59 QDP
↳60 UsableRulesProof (⇔, 0 ms)
↳61 QDP
↳62 QReductionProof (⇔, 2 ms)
↳63 QDP
↳64 Narrowing (⇒, 0 ms)
↳65 QDP
↳66 UsableRulesProof (⇔, 0 ms)
↳67 QDP
↳68 QReductionProof (⇔, 8 ms)
↳69 QDP
↳70 Rewriting (⇔, 21 ms)
↳71 QDP
↳72 UsableRulesProof (⇔, 0 ms)
↳73 QDP
↳74 QReductionProof (⇔, 33 ms)
↳75 QDP
↳76 Rewriting (⇔, 0 ms)
↳77 QDP
↳78 UsableRulesProof (⇔, 0 ms)
↳79 QDP
↳80 QReductionProof (⇔, 31 ms)
↳81 QDP
↳82 QDPOrderProof (⇔, 226 ms)
↳83 QDP
↳84 MRRProof (⇔, 361 ms)
↳85 QDP
↳86 DependencyGraphProof (⇔, 0 ms)
↳87 QDP
↳88 QReductionProof (⇔, 0 ms)
↳89 QDP
↳90 MRRProof (⇔, 160 ms)
↳91 QDP
↳92 DependencyGraphProof (⇔, 0 ms)
↳93 TRUE
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → U11_GA(T17, T18, delE_in_ga(T17, X14))
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → DELE_IN_GA(T17, X14)
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, delE_in_ga(T17, T21))
U12_GA(T17, T18, delE_out_ga(T17, T21)) → U13_GA(T17, T18, maxsortJ_in_ga(T21, T18))
U12_GA(T17, T18, delE_out_ga(T17, T21)) → MAXSORTJ_IN_GA(T21, T18)
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T55, T56)) → U14_GA(T53, T55, T56, maxA_in_ga(T53, T55))
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T55, T56)) → MAXA_IN_GA(T53, T55)
MAXA_IN_GA(.(t, T72), T74) → U1_GA(T72, T74, maxA_in_ga(T72, T74))
MAXA_IN_GA(.(t, T72), T74) → MAXA_IN_GA(T72, T74)
MAXA_IN_GA(.(f, T72), T74) → U2_GA(T72, T74, maxA_in_ga(T72, T74))
MAXA_IN_GA(.(f, T72), T74) → MAXA_IN_GA(T72, T74)
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T57, T58)) → U15_GA(T53, T57, T58, maxA_in_ga(T53, T57))
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_GA(T53, T57, T58, delF_in_gga(T57, T53, X14))
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → DELF_IN_GGA(T57, T53, X14)
DELF_IN_GGA(f, T118, .(t, .(t, X187))) → U7_GGA(T118, X187, delB_in_ga(T118, X187))
DELF_IN_GGA(f, T118, .(t, .(t, X187))) → DELB_IN_GA(T118, X187)
DELB_IN_GA(.(t, T134), .(t, X228)) → U3_GA(T134, X228, delB_in_ga(T134, X228))
DELB_IN_GA(.(t, T134), .(t, X228)) → DELB_IN_GA(T134, X228)
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_GA(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_GA(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_GA(T53, T57, T58, maxsortJ_in_ga(T87, T58))
U17_GA(T53, T57, T58, delF_out_gga(T57, T53, T87)) → MAXSORTJ_IN_GA(T87, T58)
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T55, T56)) → U19_GA(T53, T55, T56, maxA_in_ga(T53, T55))
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T55, T56)) → MAXA_IN_GA(T53, T55)
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T135, T136)) → U20_GA(T53, T135, T136, maxA_in_ga(T53, T135))
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_GA(T53, T135, T136, delG_in_gga(T135, T53, X14))
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → DELG_IN_GGA(T135, T53, X14)
DELG_IN_GGA(f, T160, .(t, X269)) → U8_GGA(T160, X269, delB_in_ga(.(f, T160), X269))
DELG_IN_GGA(f, T160, .(t, X269)) → DELB_IN_GA(.(f, T160), X269)
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_GA(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_GA(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_GA(T53, T135, T136, maxsortJ_in_ga(T139, T136))
U22_GA(T53, T135, T136, delG_out_gga(T135, T53, T139)) → MAXSORTJ_IN_GA(T139, T136)
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T55, T56)) → U24_GA(T53, T55, T56, maxC_in_ga(T53, T55))
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T55, T56)) → MAXC_IN_GA(T53, T55)
MAXC_IN_GA(.(f, T178), T180) → U4_GA(T178, T180, maxC_in_ga(T178, T180))
MAXC_IN_GA(.(f, T178), T180) → MAXC_IN_GA(T178, T180)
MAXC_IN_GA(.(t, T188), T190) → U5_GA(T188, T190, maxA_in_ga(T188, T190))
MAXC_IN_GA(.(t, T188), T190) → MAXA_IN_GA(T188, T190)
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T163, T164)) → U25_GA(T53, T163, T164, maxC_in_ga(T53, T163))
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_GA(T53, T163, T164, delH_in_gga(T163, T53, X14))
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → DELH_IN_GGA(T163, T53, X14)
DELH_IN_GGA(t, T224, .(f, .(f, X384))) → U9_GGA(T224, X384, delD_in_ga(T224, X384))
DELH_IN_GGA(t, T224, .(f, .(f, X384))) → DELD_IN_GA(T224, X384)
DELD_IN_GA(.(f, T240), .(f, X427)) → U6_GA(T240, X427, delD_in_ga(T240, X427))
DELD_IN_GA(.(f, T240), .(f, X427)) → DELD_IN_GA(T240, X427)
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_GA(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_GA(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_GA(T53, T163, T164, maxsortJ_in_ga(T193, T164))
U27_GA(T53, T163, T164, delH_out_gga(T163, T53, T193)) → MAXSORTJ_IN_GA(T193, T164)
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T253, T254)) → U29_GA(T251, T253, T254, maxA_in_ga(T251, T253))
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T253, T254)) → MAXA_IN_GA(T251, T253)
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T255, T256)) → U30_GA(T251, T255, T256, maxA_in_ga(T251, T255))
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_GA(T251, T255, T256, delI_in_gga(T255, T251, X14))
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → DELI_IN_GGA(T255, T251, X14)
DELI_IN_GGA(t, T280, .(f, X480)) → U10_GGA(T280, X480, delD_in_ga(.(t, T280), X480))
DELI_IN_GGA(t, T280, .(f, X480)) → DELD_IN_GA(.(t, T280), X480)
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_GA(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_GA(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_GA(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U32_GA(T251, T255, T256, delI_out_gga(T255, T251, T259)) → MAXSORTJ_IN_GA(T259, T256)
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → U11_GA(T17, T18, delE_in_ga(T17, X14))
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → DELE_IN_GA(T17, X14)
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, delE_in_ga(T17, T21))
U12_GA(T17, T18, delE_out_ga(T17, T21)) → U13_GA(T17, T18, maxsortJ_in_ga(T21, T18))
U12_GA(T17, T18, delE_out_ga(T17, T21)) → MAXSORTJ_IN_GA(T21, T18)
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T55, T56)) → U14_GA(T53, T55, T56, maxA_in_ga(T53, T55))
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T55, T56)) → MAXA_IN_GA(T53, T55)
MAXA_IN_GA(.(t, T72), T74) → U1_GA(T72, T74, maxA_in_ga(T72, T74))
MAXA_IN_GA(.(t, T72), T74) → MAXA_IN_GA(T72, T74)
MAXA_IN_GA(.(f, T72), T74) → U2_GA(T72, T74, maxA_in_ga(T72, T74))
MAXA_IN_GA(.(f, T72), T74) → MAXA_IN_GA(T72, T74)
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T57, T58)) → U15_GA(T53, T57, T58, maxA_in_ga(T53, T57))
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_GA(T53, T57, T58, delF_in_gga(T57, T53, X14))
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → DELF_IN_GGA(T57, T53, X14)
DELF_IN_GGA(f, T118, .(t, .(t, X187))) → U7_GGA(T118, X187, delB_in_ga(T118, X187))
DELF_IN_GGA(f, T118, .(t, .(t, X187))) → DELB_IN_GA(T118, X187)
DELB_IN_GA(.(t, T134), .(t, X228)) → U3_GA(T134, X228, delB_in_ga(T134, X228))
DELB_IN_GA(.(t, T134), .(t, X228)) → DELB_IN_GA(T134, X228)
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_GA(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_GA(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_GA(T53, T57, T58, maxsortJ_in_ga(T87, T58))
U17_GA(T53, T57, T58, delF_out_gga(T57, T53, T87)) → MAXSORTJ_IN_GA(T87, T58)
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T55, T56)) → U19_GA(T53, T55, T56, maxA_in_ga(T53, T55))
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T55, T56)) → MAXA_IN_GA(T53, T55)
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T135, T136)) → U20_GA(T53, T135, T136, maxA_in_ga(T53, T135))
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_GA(T53, T135, T136, delG_in_gga(T135, T53, X14))
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → DELG_IN_GGA(T135, T53, X14)
DELG_IN_GGA(f, T160, .(t, X269)) → U8_GGA(T160, X269, delB_in_ga(.(f, T160), X269))
DELG_IN_GGA(f, T160, .(t, X269)) → DELB_IN_GA(.(f, T160), X269)
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_GA(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_GA(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_GA(T53, T135, T136, maxsortJ_in_ga(T139, T136))
U22_GA(T53, T135, T136, delG_out_gga(T135, T53, T139)) → MAXSORTJ_IN_GA(T139, T136)
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T55, T56)) → U24_GA(T53, T55, T56, maxC_in_ga(T53, T55))
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T55, T56)) → MAXC_IN_GA(T53, T55)
MAXC_IN_GA(.(f, T178), T180) → U4_GA(T178, T180, maxC_in_ga(T178, T180))
MAXC_IN_GA(.(f, T178), T180) → MAXC_IN_GA(T178, T180)
MAXC_IN_GA(.(t, T188), T190) → U5_GA(T188, T190, maxA_in_ga(T188, T190))
MAXC_IN_GA(.(t, T188), T190) → MAXA_IN_GA(T188, T190)
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T163, T164)) → U25_GA(T53, T163, T164, maxC_in_ga(T53, T163))
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_GA(T53, T163, T164, delH_in_gga(T163, T53, X14))
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → DELH_IN_GGA(T163, T53, X14)
DELH_IN_GGA(t, T224, .(f, .(f, X384))) → U9_GGA(T224, X384, delD_in_ga(T224, X384))
DELH_IN_GGA(t, T224, .(f, .(f, X384))) → DELD_IN_GA(T224, X384)
DELD_IN_GA(.(f, T240), .(f, X427)) → U6_GA(T240, X427, delD_in_ga(T240, X427))
DELD_IN_GA(.(f, T240), .(f, X427)) → DELD_IN_GA(T240, X427)
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_GA(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_GA(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_GA(T53, T163, T164, maxsortJ_in_ga(T193, T164))
U27_GA(T53, T163, T164, delH_out_gga(T163, T53, T193)) → MAXSORTJ_IN_GA(T193, T164)
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T253, T254)) → U29_GA(T251, T253, T254, maxA_in_ga(T251, T253))
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T253, T254)) → MAXA_IN_GA(T251, T253)
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T255, T256)) → U30_GA(T251, T255, T256, maxA_in_ga(T251, T255))
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_GA(T251, T255, T256, delI_in_gga(T255, T251, X14))
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → DELI_IN_GGA(T255, T251, X14)
DELI_IN_GGA(t, T280, .(f, X480)) → U10_GGA(T280, X480, delD_in_ga(.(t, T280), X480))
DELI_IN_GGA(t, T280, .(f, X480)) → DELD_IN_GA(.(t, T280), X480)
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_GA(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_GA(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_GA(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U32_GA(T251, T255, T256, delI_out_gga(T255, T251, T259)) → MAXSORTJ_IN_GA(T259, T256)
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
DELD_IN_GA(.(f, T240), .(f, X427)) → DELD_IN_GA(T240, X427)
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
DELD_IN_GA(.(f, T240), .(f, X427)) → DELD_IN_GA(T240, X427)
DELD_IN_GA(.(f, T240)) → DELD_IN_GA(T240)
From the DPs we obtained the following set of size-change graphs:
DELB_IN_GA(.(t, T134), .(t, X228)) → DELB_IN_GA(T134, X228)
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
DELB_IN_GA(.(t, T134), .(t, X228)) → DELB_IN_GA(T134, X228)
DELB_IN_GA(.(t, T134)) → DELB_IN_GA(T134)
From the DPs we obtained the following set of size-change graphs:
MAXA_IN_GA(.(f, T72), T74) → MAXA_IN_GA(T72, T74)
MAXA_IN_GA(.(t, T72), T74) → MAXA_IN_GA(T72, T74)
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
MAXA_IN_GA(.(f, T72), T74) → MAXA_IN_GA(T72, T74)
MAXA_IN_GA(.(t, T72), T74) → MAXA_IN_GA(T72, T74)
MAXA_IN_GA(.(f, T72)) → MAXA_IN_GA(T72)
MAXA_IN_GA(.(t, T72)) → MAXA_IN_GA(T72)
From the DPs we obtained the following set of size-change graphs:
MAXC_IN_GA(.(f, T178), T180) → MAXC_IN_GA(T178, T180)
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
MAXC_IN_GA(.(f, T178), T180) → MAXC_IN_GA(T178, T180)
MAXC_IN_GA(.(f, T178)) → MAXC_IN_GA(T178)
From the DPs we obtained the following set of size-change graphs:
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, delE_in_ga(T17, T21))
U12_GA(T17, T18, delE_out_ga(T17, T21)) → MAXSORTJ_IN_GA(T21, T18)
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T57, T58)) → U15_GA(T53, T57, T58, maxA_in_ga(T53, T57))
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_GA(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_GA(T53, T57, T58, delF_out_gga(T57, T53, T87)) → MAXSORTJ_IN_GA(T87, T58)
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T135, T136)) → U20_GA(T53, T135, T136, maxA_in_ga(T53, T135))
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_GA(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_GA(T53, T135, T136, delG_out_gga(T135, T53, T139)) → MAXSORTJ_IN_GA(T139, T136)
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T163, T164)) → U25_GA(T53, T163, T164, maxC_in_ga(T53, T163))
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_GA(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_GA(T53, T163, T164, delH_out_gga(T163, T53, T193)) → MAXSORTJ_IN_GA(T193, T164)
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T255, T256)) → U30_GA(T251, T255, T256, maxA_in_ga(T251, T255))
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_GA(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_GA(T251, T255, T256, delI_out_gga(T255, T251, T259)) → MAXSORTJ_IN_GA(T259, T256)
maxsortJ_in_ga([], []) → maxsortJ_out_ga([], [])
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, delE_in_ga(T17, X14))
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
U11_ga(T17, T18, delE_out_ga(T17, X14)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
maxsortJ_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, delE_in_ga(T17, T21))
U12_ga(T17, T18, delE_out_ga(T17, T21)) → U13_ga(T17, T18, maxsortJ_in_ga(T21, T18))
maxsortJ_in_ga(.(t, .(t, T53)), .(T55, T56)) → U14_ga(T53, T55, T56, maxA_in_ga(T53, T55))
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U14_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(t, T53)), .(T57, T58)) → U15_ga(T53, T57, T58, maxA_in_ga(T53, T57))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U16_ga(T53, T57, T58, delF_in_gga(T57, T53, X14))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U16_ga(T53, T57, T58, delF_out_gga(T57, T53, X14)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U15_ga(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_ga(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_ga(T53, T57, T58, delF_out_gga(T57, T53, T87)) → U18_ga(T53, T57, T58, maxsortJ_in_ga(T87, T58))
maxsortJ_in_ga(.(t, .(f, T53)), .(T55, T56)) → U19_ga(T53, T55, T56, maxA_in_ga(T53, T55))
U19_ga(T53, T55, T56, maxA_out_ga(T53, T55)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(t, .(f, T53)), .(T135, T136)) → U20_ga(T53, T135, T136, maxA_in_ga(T53, T135))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U21_ga(T53, T135, T136, delG_in_gga(T135, T53, X14))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U21_ga(T53, T135, T136, delG_out_gga(T135, T53, X14)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U20_ga(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_ga(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_ga(T53, T135, T136, delG_out_gga(T135, T53, T139)) → U23_ga(T53, T135, T136, maxsortJ_in_ga(T139, T136))
maxsortJ_in_ga(.(f, .(f, T53)), .(T55, T56)) → U24_ga(T53, T55, T56, maxC_in_ga(T53, T55))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U24_ga(T53, T55, T56, maxC_out_ga(T53, T55)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T55, T56))
maxsortJ_in_ga(.(f, .(f, T53)), .(T163, T164)) → U25_ga(T53, T163, T164, maxC_in_ga(T53, T163))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U26_ga(T53, T163, T164, delH_in_gga(T163, T53, X14))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U26_ga(T53, T163, T164, delH_out_gga(T163, T53, X14)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U25_ga(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_ga(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_ga(T53, T163, T164, delH_out_gga(T163, T53, T193)) → U28_ga(T53, T163, T164, maxsortJ_in_ga(T193, T164))
maxsortJ_in_ga(.(f, .(t, T251)), .(T253, T254)) → U29_ga(T251, T253, T254, maxA_in_ga(T251, T253))
U29_ga(T251, T253, T254, maxA_out_ga(T251, T253)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T253, T254))
maxsortJ_in_ga(.(f, .(t, T251)), .(T255, T256)) → U30_ga(T251, T255, T256, maxA_in_ga(T251, T255))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U31_ga(T251, T255, T256, delI_in_gga(T255, T251, X14))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
U31_ga(T251, T255, T256, delI_out_gga(T255, T251, X14)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U30_ga(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_ga(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_ga(T251, T255, T256, delI_out_gga(T255, T251, T259)) → U33_ga(T251, T255, T256, maxsortJ_in_ga(T259, T256))
U33_ga(T251, T255, T256, maxsortJ_out_ga(T259, T256)) → maxsortJ_out_ga(.(f, .(t, T251)), .(T255, T256))
U28_ga(T53, T163, T164, maxsortJ_out_ga(T193, T164)) → maxsortJ_out_ga(.(f, .(f, T53)), .(T163, T164))
U23_ga(T53, T135, T136, maxsortJ_out_ga(T139, T136)) → maxsortJ_out_ga(.(t, .(f, T53)), .(T135, T136))
U18_ga(T53, T57, T58, maxsortJ_out_ga(T87, T58)) → maxsortJ_out_ga(.(t, .(t, T53)), .(T57, T58))
U13_ga(T17, T18, maxsortJ_out_ga(T21, T18)) → maxsortJ_out_ga(.(T17, []), .(T17, T18))
MAXSORTJ_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, delE_in_ga(T17, T21))
U12_GA(T17, T18, delE_out_ga(T17, T21)) → MAXSORTJ_IN_GA(T21, T18)
MAXSORTJ_IN_GA(.(t, .(t, T53)), .(T57, T58)) → U15_GA(T53, T57, T58, maxA_in_ga(T53, T57))
U15_GA(T53, T57, T58, maxA_out_ga(T53, T57)) → U17_GA(T53, T57, T58, delF_in_gga(T57, T53, T87))
U17_GA(T53, T57, T58, delF_out_gga(T57, T53, T87)) → MAXSORTJ_IN_GA(T87, T58)
MAXSORTJ_IN_GA(.(t, .(f, T53)), .(T135, T136)) → U20_GA(T53, T135, T136, maxA_in_ga(T53, T135))
U20_GA(T53, T135, T136, maxA_out_ga(T53, T135)) → U22_GA(T53, T135, T136, delG_in_gga(T135, T53, T139))
U22_GA(T53, T135, T136, delG_out_gga(T135, T53, T139)) → MAXSORTJ_IN_GA(T139, T136)
MAXSORTJ_IN_GA(.(f, .(f, T53)), .(T163, T164)) → U25_GA(T53, T163, T164, maxC_in_ga(T53, T163))
U25_GA(T53, T163, T164, maxC_out_ga(T53, T163)) → U27_GA(T53, T163, T164, delH_in_gga(T163, T53, T193))
U27_GA(T53, T163, T164, delH_out_gga(T163, T53, T193)) → MAXSORTJ_IN_GA(T193, T164)
MAXSORTJ_IN_GA(.(f, .(t, T251)), .(T255, T256)) → U30_GA(T251, T255, T256, maxA_in_ga(T251, T255))
U30_GA(T251, T255, T256, maxA_out_ga(T251, T255)) → U32_GA(T251, T255, T256, delI_in_gga(T255, T251, T259))
U32_GA(T251, T255, T256, delI_out_gga(T255, T251, T259)) → MAXSORTJ_IN_GA(T259, T256)
delE_in_ga(t, []) → delE_out_ga(t, [])
delE_in_ga(f, []) → delE_out_ga(f, [])
maxA_in_ga([], t) → maxA_out_ga([], t)
maxA_in_ga(.(t, T72), T74) → U1_ga(T72, T74, maxA_in_ga(T72, T74))
maxA_in_ga(.(f, T72), T74) → U2_ga(T72, T74, maxA_in_ga(T72, T74))
delF_in_gga(t, T100, .(t, T100)) → delF_out_gga(t, T100, .(t, T100))
delF_in_gga(f, T118, .(t, .(t, X187))) → U7_gga(T118, X187, delB_in_ga(T118, X187))
delG_in_gga(t, T152, .(f, T152)) → delG_out_gga(t, T152, .(f, T152))
delG_in_gga(f, T160, .(t, X269)) → U8_gga(T160, X269, delB_in_ga(.(f, T160), X269))
maxC_in_ga([], f) → maxC_out_ga([], f)
maxC_in_ga(.(f, T178), T180) → U4_ga(T178, T180, maxC_in_ga(T178, T180))
maxC_in_ga(.(t, T188), T190) → U5_ga(T188, T190, maxA_in_ga(T188, T190))
delH_in_gga(f, T206, .(f, T206)) → delH_out_gga(f, T206, .(f, T206))
delH_in_gga(t, T224, .(f, .(f, X384))) → U9_gga(T224, X384, delD_in_ga(T224, X384))
delI_in_gga(f, T272, .(t, T272)) → delI_out_gga(f, T272, .(t, T272))
delI_in_gga(t, T280, .(f, X480)) → U10_gga(T280, X480, delD_in_ga(.(t, T280), X480))
U1_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(t, T72), T74)
U2_ga(T72, T74, maxA_out_ga(T72, T74)) → maxA_out_ga(.(f, T72), T74)
U7_gga(T118, X187, delB_out_ga(T118, X187)) → delF_out_gga(f, T118, .(t, .(t, X187)))
U8_gga(T160, X269, delB_out_ga(.(f, T160), X269)) → delG_out_gga(f, T160, .(t, X269))
U4_ga(T178, T180, maxC_out_ga(T178, T180)) → maxC_out_ga(.(f, T178), T180)
U5_ga(T188, T190, maxA_out_ga(T188, T190)) → maxC_out_ga(.(t, T188), T190)
U9_gga(T224, X384, delD_out_ga(T224, X384)) → delH_out_gga(t, T224, .(f, .(f, X384)))
U10_gga(T280, X480, delD_out_ga(.(t, T280), X480)) → delI_out_gga(t, T280, .(f, X480))
delB_in_ga([], []) → delB_out_ga([], [])
delB_in_ga(.(f, T128), T128) → delB_out_ga(.(f, T128), T128)
delB_in_ga(.(t, T134), .(t, X228)) → U3_ga(T134, X228, delB_in_ga(T134, X228))
delD_in_ga([], []) → delD_out_ga([], [])
delD_in_ga(.(t, T234), T234) → delD_out_ga(.(t, T234), T234)
delD_in_ga(.(f, T240), .(f, X427)) → U6_ga(T240, X427, delD_in_ga(T240, X427))
U3_ga(T134, X228, delB_out_ga(T134, X228)) → delB_out_ga(.(t, T134), .(t, X228))
U6_ga(T240, X427, delD_out_ga(T240, X427)) → delD_out_ga(.(f, T240), .(f, X427))
MAXSORTJ_IN_GA(.(T17, [])) → U12_GA(delE_in_ga(T17))
U12_GA(delE_out_ga(T21)) → MAXSORTJ_IN_GA(T21)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delE_in_ga(t) → delE_out_ga([])
delE_in_ga(f) → delE_out_ga([])
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
delF_in_gga(f, T118) → U7_gga(delB_in_ga(T118))
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U7_gga(delB_out_ga(X187)) → delF_out_gga(.(t, .(t, X187)))
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
delB_in_ga([]) → delB_out_ga([])
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
delB_in_ga(.(t, T134)) → U3_ga(delB_in_ga(T134))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U3_ga(delB_out_ga(X228)) → delB_out_ga(.(t, X228))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
delE_in_ga(x0)
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
MAXSORTJ_IN_GA(.(t, [])) → U12_GA(delE_out_ga([]))
MAXSORTJ_IN_GA(.(f, [])) → U12_GA(delE_out_ga([]))
U12_GA(delE_out_ga(T21)) → MAXSORTJ_IN_GA(T21)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
MAXSORTJ_IN_GA(.(t, [])) → U12_GA(delE_out_ga([]))
MAXSORTJ_IN_GA(.(f, [])) → U12_GA(delE_out_ga([]))
delE_in_ga(t) → delE_out_ga([])
delE_in_ga(f) → delE_out_ga([])
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
delF_in_gga(f, T118) → U7_gga(delB_in_ga(T118))
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U7_gga(delB_out_ga(X187)) → delF_out_gga(.(t, .(t, X187)))
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
delB_in_ga([]) → delB_out_ga([])
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
delB_in_ga(.(t, T134)) → U3_ga(delB_in_ga(T134))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U3_ga(delB_out_ga(X228)) → delB_out_ga(.(t, X228))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
delE_in_ga(x0)
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
U12_GA(delE_out_ga(T21)) → MAXSORTJ_IN_GA(T21)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
MAXSORTJ_IN_GA(.(t, [])) → U12_GA(delE_out_ga([]))
MAXSORTJ_IN_GA(.(f, [])) → U12_GA(delE_out_ga([]))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
delF_in_gga(f, T118) → U7_gga(delB_in_ga(T118))
delB_in_ga([]) → delB_out_ga([])
delB_in_ga(.(t, T134)) → U3_ga(delB_in_ga(T134))
U7_gga(delB_out_ga(X187)) → delF_out_gga(.(t, .(t, X187)))
U3_ga(delB_out_ga(X228)) → delB_out_ga(.(t, X228))
delE_in_ga(x0)
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
delE_in_ga(x0)
U12_GA(delE_out_ga(T21)) → MAXSORTJ_IN_GA(T21)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
MAXSORTJ_IN_GA(.(t, [])) → U12_GA(delE_out_ga([]))
MAXSORTJ_IN_GA(.(f, [])) → U12_GA(delE_out_ga([]))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
delF_in_gga(f, T118) → U7_gga(delB_in_ga(T118))
delB_in_ga([]) → delB_out_ga([])
delB_in_ga(.(t, T134)) → U3_ga(delB_in_ga(T134))
U7_gga(delB_out_ga(X187)) → delF_out_gga(.(t, .(t, X187)))
U3_ga(delB_out_ga(X228)) → delB_out_ga(.(t, X228))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
U12_GA(delE_out_ga([])) → MAXSORTJ_IN_GA([])
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
MAXSORTJ_IN_GA(.(t, [])) → U12_GA(delE_out_ga([]))
MAXSORTJ_IN_GA(.(f, [])) → U12_GA(delE_out_ga([]))
U12_GA(delE_out_ga([])) → MAXSORTJ_IN_GA([])
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
delF_in_gga(f, T118) → U7_gga(delB_in_ga(T118))
delB_in_ga([]) → delB_out_ga([])
delB_in_ga(.(t, T134)) → U3_ga(delB_in_ga(T134))
U7_gga(delB_out_ga(X187)) → delF_out_gga(.(t, .(t, X187)))
U3_ga(delB_out_ga(X228)) → delB_out_ga(.(t, X228))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
delF_in_gga(f, T118) → U7_gga(delB_in_ga(T118))
delB_in_ga([]) → delB_out_ga([])
delB_in_ga(.(t, T134)) → U3_ga(delB_in_ga(T134))
U7_gga(delB_out_ga(X187)) → delF_out_gga(.(t, .(t, X187)))
U3_ga(delB_out_ga(X228)) → delB_out_ga(.(t, X228))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
delF_in_gga(f, T118) → U7_gga(delB_in_ga(T118))
POL(.(x1, x2)) = 0
POL(MAXSORTJ_IN_GA(x1)) = 0
POL(U10_gga(x1)) = 1
POL(U15_GA(x1, x2)) = 2·x2
POL(U17_GA(x1)) = 2·x1
POL(U1_ga(x1)) = 2·x1
POL(U20_GA(x1, x2)) = 0
POL(U22_GA(x1)) = 0
POL(U25_GA(x1, x2)) = 0
POL(U27_GA(x1)) = 0
POL(U2_ga(x1)) = 2·x1
POL(U30_GA(x1, x2)) = 0
POL(U32_GA(x1)) = 0
POL(U3_ga(x1)) = 0
POL(U4_ga(x1)) = 1
POL(U5_ga(x1)) = x1
POL(U6_ga(x1)) = 2
POL(U7_gga(x1)) = x1
POL(U8_gga(x1)) = 0
POL(U9_gga(x1)) = 0
POL([]) = 1
POL(delB_in_ga(x1)) = 0
POL(delB_out_ga(x1)) = 0
POL(delD_in_ga(x1)) = 2
POL(delD_out_ga(x1)) = 0
POL(delF_in_gga(x1, x2)) = x1
POL(delF_out_gga(x1)) = 2·x1
POL(delG_in_gga(x1, x2)) = 2 + x1
POL(delG_out_gga(x1)) = 0
POL(delH_in_gga(x1, x2)) = 2 + 2·x2
POL(delH_out_gga(x1)) = x1
POL(delI_in_gga(x1, x2)) = 2
POL(delI_out_gga(x1)) = 0
POL(f) = 1
POL(maxA_in_ga(x1)) = 0
POL(maxA_out_ga(x1)) = x1
POL(maxC_in_ga(x1)) = 2
POL(maxC_out_ga(x1)) = 0
POL(t) = 0
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
delB_in_ga([]) → delB_out_ga([])
delB_in_ga(.(t, T134)) → U3_ga(delB_in_ga(T134))
U7_gga(delB_out_ga(X187)) → delF_out_gga(.(t, .(t, X187)))
U3_ga(delB_out_ga(X228)) → delB_out_ga(.(t, X228))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
U7_gga(x0)
U3_ga(x0)
U15_GA(T53, maxA_out_ga(T57)) → U17_GA(delF_in_gga(T57, T53))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delF_in_gga(t, T100) → delF_out_gga(.(t, T100))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
maxA_in_ga(x0)
delF_in_gga(x0, x1)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
delF_in_gga(x0, x1)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U20_GA(T53, maxA_out_ga(T135)) → U22_GA(delG_in_gga(T135, T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
maxA_in_ga(x0)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_in_ga(.(f, x0))))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_in_ga(.(f, x0))))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
delG_in_gga(t, T152) → delG_out_gga(.(f, T152))
delG_in_gga(f, T160) → U8_gga(delB_in_ga(.(f, T160)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
maxA_in_ga(x0)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_in_ga(.(f, x0))))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
delG_in_gga(x0, x1)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
delG_in_gga(x0, x1)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_in_ga(.(f, x0))))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_out_ga(x0)))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_out_ga(x0)))
delB_in_ga(.(f, T128)) → delB_out_ga(T128)
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_out_ga(x0)))
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delB_in_ga(x0)
delD_in_ga(x0)
U6_ga(x0)
delB_in_ga(x0)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(U8_gga(delB_out_ga(x0)))
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
U20_GA(x0, maxA_out_ga(f)) → U22_GA(delG_out_gga(.(t, x0)))
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(delG_out_gga(.(t, x0)))
U8_gga(delB_out_ga(X269)) → delG_out_gga(.(t, X269))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(delG_out_gga(.(t, x0)))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
U8_gga(x0)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
U20_GA(x0, maxA_out_ga(f)) → U22_GA(delG_out_gga(.(t, x0)))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U20_GA(x0, maxA_out_ga(f)) → U22_GA(delG_out_gga(.(t, x0)))
POL(.(x1, x2)) = x2
POL(MAXSORTJ_IN_GA(x1)) = 0
POL(U10_gga(x1)) = 0
POL(U15_GA(x1, x2)) = 0
POL(U17_GA(x1)) = 0
POL(U1_ga(x1)) = x1
POL(U20_GA(x1, x2)) = x2
POL(U22_GA(x1)) = 0
POL(U25_GA(x1, x2)) = 0
POL(U27_GA(x1)) = 0
POL(U2_ga(x1)) = x1
POL(U30_GA(x1, x2)) = 0
POL(U32_GA(x1)) = 0
POL(U4_ga(x1)) = 0
POL(U5_ga(x1)) = 0
POL(U6_ga(x1)) = 0
POL(U9_gga(x1)) = 0
POL([]) = 0
POL(delD_in_ga(x1)) = 1 + x1
POL(delD_out_ga(x1)) = 0
POL(delF_out_gga(x1)) = 0
POL(delG_out_gga(x1)) = 0
POL(delH_in_gga(x1, x2)) = 0
POL(delH_out_gga(x1)) = 0
POL(delI_in_gga(x1, x2)) = 0
POL(delI_out_gga(x1)) = 0
POL(f) = 1
POL(maxA_in_ga(x1)) = 0
POL(maxA_out_ga(x1)) = x1
POL(maxC_in_ga(x1)) = 0
POL(maxC_out_ga(x1)) = 0
POL(t) = 0
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
MAXSORTJ_IN_GA(.(t, .(t, T53))) → U15_GA(T53, maxA_in_ga(T53))
MAXSORTJ_IN_GA(.(t, .(f, T53))) → U20_GA(T53, maxA_in_ga(T53))
delI_in_gga(t, T280) → U10_gga(delD_in_ga(.(t, T280)))
delD_in_ga(.(t, T234)) → delD_out_ga(T234)
U10_gga(delD_out_ga(X480)) → delI_out_gga(.(f, X480))
maxA_in_ga(.(t, T72)) → U1_ga(maxA_in_ga(T72))
U1_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
U9_gga(delD_out_ga(X384)) → delH_out_gga(.(f, .(f, X384)))
maxC_in_ga(.(t, T188)) → U5_ga(maxA_in_ga(T188))
U5_ga(maxA_out_ga(T190)) → maxC_out_ga(T190)
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(MAXSORTJ_IN_GA(x1)) = 2 + x1
POL(U10_gga(x1)) = 1 + x1
POL(U15_GA(x1, x2)) = 2·x1 + 2·x2
POL(U17_GA(x1)) = 1 + x1
POL(U1_ga(x1)) = 1 + x1
POL(U20_GA(x1, x2)) = 2·x1 + x2
POL(U22_GA(x1)) = 1 + x1
POL(U25_GA(x1, x2)) = 1 + 2·x1 + x2
POL(U27_GA(x1)) = 1 + x1
POL(U2_ga(x1)) = x1
POL(U30_GA(x1, x2)) = 2 + 2·x1 + 2·x2
POL(U32_GA(x1)) = 2 + x1
POL(U4_ga(x1)) = x1
POL(U5_ga(x1)) = 2 + x1
POL(U6_ga(x1)) = 2·x1
POL(U9_gga(x1)) = 2 + 2·x1
POL([]) = 0
POL(delD_in_ga(x1)) = x1
POL(delD_out_ga(x1)) = 2·x1
POL(delF_out_gga(x1)) = 1 + x1
POL(delG_out_gga(x1)) = 1 + x1
POL(delH_in_gga(x1, x2)) = 1 + x1 + 2·x2
POL(delH_out_gga(x1)) = 1 + x1
POL(delI_in_gga(x1, x2)) = 2 + 2·x1 + 2·x2
POL(delI_out_gga(x1)) = x1
POL(f) = 0
POL(maxA_in_ga(x1)) = 2 + x1
POL(maxA_out_ga(x1)) = 1 + x1
POL(maxC_in_ga(x1)) = 1 + 2·x1
POL(maxC_out_ga(x1)) = 1 + x1
POL(t) = 1
U17_GA(delF_out_gga(T87)) → MAXSORTJ_IN_GA(T87)
U22_GA(delG_out_gga(T139)) → MAXSORTJ_IN_GA(T139)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
U15_GA(x0, maxA_out_ga(t)) → U17_GA(delF_out_gga(.(t, x0)))
U20_GA(x0, maxA_out_ga(t)) → U22_GA(delG_out_gga(.(f, x0)))
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
U1_ga(x0)
U5_ga(x0)
U10_gga(x0)
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
maxA_in_ga([]) → maxA_out_ga(t)
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga([]) → delD_out_ga([])
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U2_ga(x0)
U4_ga(x0)
U9_gga(x0)
delD_in_ga(x0)
U6_ga(x0)
MAXSORTJ_IN_GA(.(f, .(f, T53))) → U25_GA(T53, maxC_in_ga(T53))
U32_GA(delI_out_gga(T259)) → MAXSORTJ_IN_GA(T259)
delI_in_gga(f, T272) → delI_out_gga(.(t, T272))
maxA_in_ga([]) → maxA_out_ga(t)
U2_ga(maxA_out_ga(T74)) → maxA_out_ga(T74)
delH_in_gga(t, T224) → U9_gga(delD_in_ga(T224))
delD_in_ga(.(f, T240)) → U6_ga(delD_in_ga(T240))
U6_ga(delD_out_ga(X427)) → delD_out_ga(.(f, X427))
U4_ga(maxC_out_ga(T180)) → maxC_out_ga(T180)
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(MAXSORTJ_IN_GA(x1)) = 1 + x1
POL(U25_GA(x1, x2)) = 2 + 2·x1 + 2·x2
POL(U27_GA(x1)) = 1 + x1
POL(U2_ga(x1)) = 2·x1
POL(U30_GA(x1, x2)) = 1 + 2·x1 + x2
POL(U32_GA(x1)) = 1 + x1
POL(U4_ga(x1)) = 2 + 2·x1
POL(U6_ga(x1)) = 2 + 2·x1
POL(U9_gga(x1)) = x1
POL([]) = 1
POL(delD_in_ga(x1)) = 2·x1
POL(delD_out_ga(x1)) = 1 + x1
POL(delH_in_gga(x1, x2)) = 1 + x1 + 2·x2
POL(delH_out_gga(x1)) = x1
POL(delI_in_gga(x1, x2)) = 2 + 2·x1 + 2·x2
POL(delI_out_gga(x1)) = 2 + x1
POL(f) = 1
POL(maxA_in_ga(x1)) = 2 + x1
POL(maxA_out_ga(x1)) = 2 + 2·x1
POL(maxC_in_ga(x1)) = x1
POL(maxC_out_ga(x1)) = x1
POL(t) = 0
U25_GA(T53, maxC_out_ga(T163)) → U27_GA(delH_in_gga(T163, T53))
U27_GA(delH_out_gga(T193)) → MAXSORTJ_IN_GA(T193)
MAXSORTJ_IN_GA(.(f, .(t, T251))) → U30_GA(T251, maxA_in_ga(T251))
U30_GA(T251, maxA_out_ga(T255)) → U32_GA(delI_in_gga(T255, T251))
maxA_in_ga(.(f, T72)) → U2_ga(maxA_in_ga(T72))
delH_in_gga(f, T206) → delH_out_gga(.(f, T206))
delD_in_ga([]) → delD_out_ga([])
maxC_in_ga([]) → maxC_out_ga(f)
maxC_in_ga(.(f, T178)) → U4_ga(maxC_in_ga(T178))
maxA_in_ga(x0)
maxC_in_ga(x0)
delH_in_gga(x0, x1)
delI_in_gga(x0, x1)
U2_ga(x0)
U4_ga(x0)
U9_gga(x0)
delD_in_ga(x0)
U6_ga(x0)